A:Type, L:(A List), n:. (n  ||L||)  (||lastn(n;L)|| = n  ) 

latex

ProofTree

Definitions	Type, t  T, s = t, type List, , x:AB(x), x:A. B(x), ||as||, {x:A| B(x)} , , |g|, S  T, A  B, P  Q, False, A, lastn(n;L), n - m, {i...j}, -n, n+m, a < b, Void, #$n, x:A  B(x), P & Q, P  Q, P  Q
Lemmas	iff wf, rev implies wf, length nth tl, member wf, le wf, length wf1, nat wf